the_w:World, l:IdLnk, t:. queue(l;t)  Msg List 

latex

Definitions	queue(l;t), nth_tl(n;as), Msg, snds(l;t), ||as||, Action(i), destination(l), rcvs(l;t), x:A. B(x), , IdLnk, t  T, World
Lemmas	world wf, IdLnk wf, nat wf, w-rcvs wf, ldst wf, w-action wf, length wf1, w-snds wf, w-Msg wf, nth tl wf